COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	NOTES ON AXIOMATIZING THE BLOCKS WORLD RELYING ON CIRCUMSCRIPTION
C00008 00003	THE BLOCKS WORLD IN THE SITUATION CALCULUS
C00020 00004	LIST OF AXIOMS
C00023 00005	Remarks:
C00025 ENDMK
C⊗;
NOTES ON AXIOMATIZING THE BLOCKS WORLD RELYING ON CIRCUMSCRIPTION

			by John McCarthy


INTRODUCTION

	In (McCarthy 1960), I proposed axiomatizing common sense
knowledge in some language of mathemtical logic and a program that
would decide what to do by finding a course of action that it could
deduce would achieve the goal.  (McCarthy and Hayes 1969) continued
this line of research.  It has been pointed out by me and also
in (Newell 1980) that while non-deductive problem solving methods
are more effective when they are known, it is still important to
express the common sense facts in logic.

	This isn't the place for a full discussion of these issues,
but my present position is that many efficient special programs
will be obtained by "compiling" from a logical specification of
the consequences of actions.  The logical axioms will not themselves
be a program (in Prolog or any other language) because they may
contain quantifiers and other non-effective specifications and
will usually specify the desired strategy implicitly.
The work of Goad (1981) is relevant to this.

	While ad hoc axiomatizations appropriate for solving
particular problems are not difficult to find, no-one has succeeded
in axiomatizing any substantial domain of common sense knowledge in
a general way.  A general axiomatization could be included in
a database of common sene knowledge, and when a program is confronted
with a particular problem, it would find the common sense facts about
the kinds of entities mentioned in the problem.  For example, a program
confronted with an English language version of the Missionaries and
Cannibals problem (or a translation of it directly in logic) should
look up the facts about using boats and the properties of cannibals
in the database rather than being supplied and ad hoc version by
the programmer of the problem solving system.  Not only isn't there an
axiomatization in logic of a substantial common sense domain, there
isn't a general representation of such facts in any other formalism
either.

	It has been clear for some years that the common sense reasoning
required to solve common sense problems must be non-monotonic.  The
axioms cannot contain every possible qualification of the conditions
for performing an axiom, and the reasoning program must be able to
jump to conclusions that the situation is the simplest (in some sense)
compatible with the facts being taken into account.  Ockham's razor
is used not merely in philosophical discourse, but by every person
every day of his life, and robots must use it too.  Indeed, the objections
to AI use of formalizations in logic can often be regarded as complaints about
the lack of non-monotonic reasoning in logical deduction.
See (Minsky  xx) for such argumets.

	(McCarthy 1980) proposes circumscription as mode of non-monotonic
reasoning and discusses how it may be used to be used to give more
realistic formalizations of common sense knowledge.  In this paper
we continue the discussion and try to get a general expression of
the facts about moving objects from one place to another that
would be suitable for a robot to use.  The results are an improvement
on past efforts, but sufficient generality is not achieved.  Circumscription
helps, but more improvements are needed befor the goal of a common
sense database can be realized.


THE BLOCKS WORLD IN THE SITUATION CALCULUS

	The situation calculus of (McCarthy and Hayes 1969) is inadequate
to discuss concurrent action, so it can't be the ultimate formalization.
We'll use it anyway, because nothing better is currently available for
doing the action problems wherein we can regard a new situation as the
result of taking the action in the old situation.

	We would like to describe moving by

∀ obj place. Move(obj,place) causes At(obj, place)

using

∀e p. e causes p  ⊃ ∀s.succeeds(e,s) ⊃ holds(p,result(e,s))

and using non-monotonic reasoning to determine when  Move(obj,place)
succeeds, what it changes and what remains unchanged.

	The frame problem is to be handled by

∀obj place. persistent At(obj,place)

and further non-monotonic reasoning.  In these notes we describe
what circumscriptions on what information will do the job, but we
don't yet have a fully coherent notion of how to express the common
sense knowledge in a way that insures that the right circumscriptions
will be done.


SUCCESS AND PREVENTION

∀obj place. Move(obj, place) causes At(obj, place)

∀e p. e causes p ⊃ ∀s. succeeds(e,s) ⊃ holds(p,result(e,s))

and consequently

∀obj place s. succeeds(Move(obj,place),s) 
			⊃ holds(At(obj,place),result(Move(obj,place),s)).


SUCCESS

∀obj place s. clear(top(obj),s) ∧ clear(place,s) ∧ ¬prevented(Move(obj,place),s)
		⊃ succeeds(Move(obj,place),s)

∀obj1 obj2 s. at(obj1,top(obj2),s) ⊃ unclear(obj2,s)

∀obj s. clear(obj,s) ≡ ¬unclear(obj,s)


FRAME

∀p e s. persistent p ∧ ¬changes(e,p) ∧ holds(p,s) ∧ successful(e,s)
				⊃ holds(p,result(e,s))

∀obj place place1. changes(Move(obj,place),At(obj,place1))

∀v e s.persistent1 v ∧ ¬changes1(e,v) ⊃ value(v,result(e,s)) = value(v,s)

∀obj place. persistent At(obj,place)

∀obj.persistent1 Color(obj)


PREVENTION

∀obj place s. tooheavy obj ⊃ prevented(Move(obj,place),s)

∀place place1 obj s. at(obj,place1,s) ∧ ¬close(place1,place,s)
				⊃ prevented(Move(obj,place),s)

Of course, there can be more axioms listing conditions that might
prevent moving.

∀place place1 place2 s.small(place) ∧ part(place1,place) ∧ part(place2,place)
				⊃ close(place1,place2,s)

∀obj place s.at(obj,place,s) ⊃ part(top(obj),place,s)

∀place1 place2 place3 s. part(place1,place2,s) ∧ part(place2,place3,s)
				⊃ part(place1,place3,s)


REIFICATIONS

∀obj place s. holds(At(obj,place),s) ≡ at(obj,place,s)

∀obj s.value(Color(obj),s) = color(obj,s)


THE PARTICULAR SITUATION S0

small(Table)

part(Place1,Table,S0)
part(Place2,Table,S0)
part(Place3,Table,S0)
part(Place4,Table,S0)

at(A,Place1,S0)
at(B,Place2,S0)
at(C,top(B),S0)
at(D,place5,S0)
at(E,place3,S0)

tooheavy A

color(A,S0) = Red
color(B,S0) = Red

color(C,S0) = Green ∨ color(E,S0) = Green

A ≠ B, etc.

disjoint(Place1,Place2), etc.

The last two should be obtained by some kind of non-monotonic reasoning,
but ordinary circumscription without the introduction of names won't work.
Reiter or somebody calls this "the unique names assumption".


USING CIRCUMSCRIPTION

	Suppose we want to put block  C  onto block  A  and then put
block  B  onto block  C.  The situation in question is

S2 = result(Move(B,top(C)),result(Move(C,top(A)),S0))

where  S0  is described above and is shown in the attached figure.
We want to show that

at(B,top(C),S2) ∧ at(C,top(A),S2)

in order to show success of our actions.  We also want to show that
the other blocks are unmoved.

	We must first show

succeeds(Move(C,top(A),S0)

and this requires showing

clear(top(C),S0) ∧ clear(top(A),S0) ∧ ¬prevented(Move(C,top(A)),S0).

In the following reasoning, there will be some wishful thinking, but
we shall need ways of controlling the circumscription process so that
the wishful thinking turns into reality.

We infer  clear(top(C),S0)  by circumscribing   at(obj,place,S0)  or
perhaps just  at(obj,top(C),S0)  using all the availabile facts.
It isn't clear that this will go with all available facts because some
situation that is the result of actions might be  S0, and in that
situation  top(C)  might not be clear.  It isn't reasonable to presuppose
or even prove by circumscription that  S0  is a "Garden of Eden" situation,
because this information might not be available in other case where we
want to prove such facts.

	However, if we circumscribe using
just the known instances of  at(obj,top(C),S0), there aren't any.  Indeed
the only wffs whose conclusion includes  at(obj,place,s)  are the
result-of-moving rules.

clear(top(A),S0  is obtained similarly to  clear(top(C),S0).

In order to show that  ¬prevented(Move(C,top(A)),S0)  we circumscribe
prevented(Move(C,top(A),S0).  This requires showing
¬tooheavy(C)  which is also done by circumscription.
This at least is easy, since the only statement in which  tooheavy
occurs positively is  tooheavy(A),  but of course we are using the
fact that all the blocks are distinct.

The definition of  close  and the specific facts about  part  show
that  close(top(B),top(A)).  The condition  at(obj,place1,s)  in
the condition for non-closeness preventing moving specializes to
at(C,place1,S0),  and circumscribing   at(C,place1,S0)  shows that
this is the only place  C  is at.

Thus we have the premisses needed to establish

at(C,top(A),result(Move(C,top(A)),S0)).

Now we need to show that  B  and  C are clear and close in the
resulting situation and that  B  isn't too heavy.  The latter
property is not situation dependent, so it follows by the same
argument that previously established that  C  wasn't too heavy.

To establish closeness we need to use the persistence of  at
and to circumscribe  changes(Move(obj,place),At(obj,place1)).
This formalization may not be flexible enough for some purposes,
because  changes(e,p)  is not situtation dependent.


INDUCTION

	To prove that something cannot be done or to prove something
about all things that can be done, we need some induction axiom
schemes.  We introduce  canresult(s,s'),  meaning that the situation
s'  can be obtained from the situation  s  by some sequence of actions, by

∀s.canresult(s,s)

and

∀s s' a.canresult(s,s') ⊃ canresult(s,result(a,s')),

where the variable  a  is considered to range over those events which are
actions.

Circumscribing the predicate  canresult  in these two formulas leads
to the schema

∀s.(phi(s) ∧ ∀s' a.[phi(s') ⊃ phi(result(a,s'))] ⊃ ∀s'(phi(s') ⊃ canresult(s,s')).

Presumably it is best to take it as an axiom schema rather than conjecture
it by circumscription each time it is wanted.  Doing so amounts to assuming
that the only situations that can result from  s  are those that are
the consequences of a sequence of events.  This seems to embody what we
mean by "can result".

	A notion of achievable propositional fluents will be required.  We have

∀p s.∃s'.canresult(s,s') ∧ holds(p,s') ⊃ achievable(p,s),

but this is insufficient, because a fluent  p  may be achievable even though
no specific situation in which  p  holds is achievable, because  p  may
turn out to hold no matter which of two courses of events occurs.
LIST OF AXIOMS

Actions and events:

e1:	∀e p. e causes p ⊃ ∀s. succeeds(e,s) ⊃ holds(p,result(e,s))

e2:	∀p e s. persistent p ∧ ¬changes(e,p) ∧ holds(p,s) ∧ successful(e,s)
				⊃ holds(p,result(e,s))

e3:	∀v e s.persistent1 v ∧ ¬changes1(e,v) ⊃ value(v,result(e,s)) = value(v,s)


Moving objects:

m1:	∀obj place. Move(obj, place) causes At(obj, place)

m2:	∀obj place place1. changes(Move(obj,place),At(obj,place1))

m3:	∀obj place. persistent At(obj,place)

m4:	∀obj place s. clear(top(obj),s) ∧ clear(place,s) ∧ ¬prevented(Move(obj,place),s)
		⊃ succeeds(Move(obj,place),s)

m5:	∀obj1 obj2 s. at(obj1,top(obj2),s) ⊃ unclear(obj2,s)

m6:	∀obj s. clear(obj,s) ≡ ¬unclear(obj,s)

m7:	∀obj place s. tooheavy obj ⊃ prevented(Move(obj,place),s)

m8:	∀place place1 obj s. at(obj,place1,s) ∧ ¬close(place1,place,s)
				⊃ prevented(Move(obj,place),s)

m9:	∀place place1 place2 s.small(place) ∧ part(place1,place) ∧ part(place2,place)
				⊃ close(place1,place2,s)

m10:	∀obj place s.at(obj,place,s) ⊃ part(top(obj),place,s)

m11:	∀place1 place2 place3 s. part(place1,place2,s) ∧ part(place2,place3,s)
				⊃ part(place1,place3,s)



Coloring objects:

c1:	∀obj color. Paint(obj,color) causes Equal(color(obj),color)

This requires more reification than the formalization of  Move(obj,place)  and
suggest a different formalization.  Namely,

c1':	∀obj color. assigns(Paint(obj,color),color(obj), color)

together with the general axiom

e1':	∀e v val s.assigns(e,v,val) ∧ successful(e,s) ⊃ value(v,result(e,s)) = val

analogous to axiom  e1.

c2:	∀obj.persistent1 Color(obj)


REIFICATIONS

r1:	∀x y s.holds(Equal(x,y),s) ≡ value(x,s) = value(y,s)

r2:	∀obj place s. holds(At(obj,place),s) ≡ at(obj,place,s)

r3:	∀obj s.value(Color(obj),s) = color(obj,s)
Remarks:

1. Query: Can we conclude that all iterates of a function  f  are
distinct by some kind of non-monotonic reasoning, e.g. circumscription
of some higher order predicate?

	In particular, we wish to avoid having to show that nothing more
can be learned about the situation  S0  by reasoning from
it to future situations and then back to  S0.  This is true about
the blocks world but is often not true when purpose is involved.
For example, we may reason from the fact that a person wants  x
tomorrow that he will have done  y  yesterday to make it possible.
We need to reason about what facts to take into account, and the
this reasoning probably should be based on an axiom to the effect
that the future doesn't have to be taken into account in determining
the facts about the present situation unless there is a specific
reason to do so.  In deciding what to do here, a circumscription
is required.